FDL - Nuprl Lemma : cond_equiv_to_causl

Nuprl Lemma : cond_equiv_to_causl

es:ES, R:(E

E

), P:(E

).
R =>

e,e'. (e < e')

(

x, y:E. (P(x) & P(y))

(((R(x,y))

(x = y))

(R(y,x))))

(

x, y:E. (P(x) & P(y))

((R(x,y))

(x < y)))

Definitions P Q, A c B, P Q, A, Trans(T;x,y.E(x;y)), t T, P Q, P & Q, P Q, , x:A. B(x), False

Lemmas es-causl irreflexivity, es-causle weakening, es-causl transitivity2, cond rel equivalent, event system wf, es-causl wf, es-E wf, rel implies wf